r:Rng, n:, u:|r|. (u r n)  |r| 

latex

Up	rings 1
Definitions of Statement	Rng, rxmn, e r n
Definitions	t.1, |g|, rxmn, e r n, t  T, x:A. B(x), Rng, S  T
Lemmas	rng wf, nat wf, rng car wf, mul mon of rng wf, grp car wf, nat inc, mul mon of rng wf c, mon nat op wf2